r:CRng.
IsIntegDom(r)  (0  1  |r|  & (u, v:|r|. ((u * v) = 0  |r|)  ((u = 0)  (v = 0)))) 

latex

Up	rings 1
Definitions of Statement	Rng, CRng, IsIntegDom(r), nat(r;a)
Definitions	, t  T, P  Q, P  Q, x f y, P  Q, P & Q, IsIntegDom(r), P  Q, x:A. B(x), Rng, CRng, Dec(P), False, A
Lemmas	crng wf, not wf, rng one wf, nequal wf, rng zero wf, rng times wf, rng car wf, decidable rng eq